$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $L$:($A$ List), $v$:Top, $x$:$A$. ($\uparrow$$x$ $\in$ dom($L$ $\vdash$fpf$\rightarrow$ $v$)) $\Leftarrow\!\Rightarrow$ ($x$ $\in$ $L$)